package edu.cmu.cs.erl.unitTests;

import java.util.ArrayList;
import java.util.List;

import jp.ac.kobe_u.cs.prolog.lang.JavaObjectTerm;
import jp.ac.kobe_u.cs.prolog.lang.Term;

import org.junit.Assert;
import org.junit.Test;

import edu.cmu.cs.erl.ERL;
import edu.cmu.cs.erl.ERLError;
import edu.cmu.cs.erl.ERLException;
import edu.cmu.cs.erl.Oracle;
import edu.cmu.cs.erl.TermBuilder;



public class NestingTest {

	@Test
	public void nestedForallExists() throws ERLException {
		Oracle oracle= new TestOracle();
	
		ArrayList<String> existsList = new ArrayList<String>();
		existsList.add("b");
		existsList.add("b");

		ArrayList<String> forallList = new ArrayList<String>();
		forallList.add("a");
		forallList.add("b");

		Term Z = TermBuilder.createAtomicTerm(oracle.getVariable("Z"));	
		Term existsTerm = TermBuilder.createExistsTerm(oracle, existsList, "Z", Z);
		Term forall1Term = TermBuilder.createForAllTerm(oracle, forallList, "Y", existsTerm);
		Term forall2Term = TermBuilder.createForAllTerm(oracle, forallList, "X", forall1Term);
	
		List<ERLError> errors = ERL.runPredicate(oracle, forall2Term, true);
		
		Assert.assertEquals(4, errors.size());
	}
	
	@Test
	public void nestedForallExistsEmpty() throws ERLException {
		Oracle oracle= new TestOracle();
	
		ArrayList<String> existsList = new ArrayList<String>();
		existsList.add("b");
		existsList.add("b");

		ArrayList<String> forallList = new ArrayList<String>();

		Term Z = TermBuilder.createAtomicTerm(oracle.getVariable("Z"));	
		Term existsTerm = TermBuilder.createExistsTerm(oracle, existsList, "Z", Z);
		Term forall1Term = TermBuilder.createForAllTerm(oracle, forallList, "Y", existsTerm);
		Term forall2Term = TermBuilder.createForAllTerm(oracle, forallList, "X", forall1Term);
	
		List<ERLError> errors = ERL.runPredicate(oracle, forall2Term, true);
		
		Assert.assertEquals(0, errors.size());
	}

	
	@Test
	public void impliesWithNestedAndExists() throws ERLException {
		Oracle oracle= new TestOracle();
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		
		Term X = TermBuilder.createAtomicTerm(oracle.getVariable("X"));	

		Term existsTerm = TermBuilder.createExistsLazyTerm(oracle, list, "X", X);
		Term andTerm = TermBuilder.createAndTerm(TermBuilder.createAtomicTerm("c"), existsTerm);
		Term impliesTerm  = TermBuilder.createImpliesTerm(TermBuilder.createAtomicTerm("a"), andTerm);

		List<ERLError> errors = ERL.runPredicate(oracle, andTerm, true);
		
		Assert.assertEquals(1, errors.size());
	}
		
	@Test
	public void impliesWithNestedAndExists2() throws ERLException {
		Oracle oracle= new TestOracle();
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("b");
		
		Term X = TermBuilder.createAtomicTerm(oracle.getVariable("X"));	

		Term existsTerm = TermBuilder.createExistsLazyTerm(oracle, list, "X", X);
		Term andTerm = TermBuilder.createAndTerm(TermBuilder.createAtomicTerm("b"), existsTerm);
		Term impliesTerm  = TermBuilder.createImpliesTerm(TermBuilder.createAtomicTerm("a"), andTerm);

		List<ERLError> errors = ERL.runPredicate(oracle, andTerm, true);
		
		Assert.assertEquals(2, errors.size());
	}
	
	@Test
	public void impliesWithNestedAndExists3() throws ERLException {
		Oracle oracle= new TestOracle();
		
		ArrayList<String> list = new ArrayList<String>();
		list.add("b");
		list.add("a");
		
		Term X = TermBuilder.createAtomicTerm(oracle.getVariable("X"));	

		Term existsTerm = TermBuilder.createExistsLazyTerm(oracle, list, "X", X);
		Term andTerm = TermBuilder.createAndTerm(TermBuilder.createAtomicTerm("b"), existsTerm);
		Term impliesTerm  = TermBuilder.createImpliesTerm(TermBuilder.createAtomicTerm("a"), andTerm);

		List<ERLError> errors = ERL.runPredicate(oracle, andTerm, true);
		
		Assert.assertEquals(1, errors.size());
	}


	
	@Test
	public void trueTest() {
		try {
			Oracle oracle = new TestOracle();
			Term orTerm = TermBuilder.createOrTerm(TermBuilder.createAtomicTerm("a"), TermBuilder.createAtomicTerm("b"));
			Term andTerm = TermBuilder.createAndTerm(TermBuilder.createAtomicTerm("a"), orTerm);
			
			List<ERLError> errors = ERL.runPredicate(oracle, andTerm, true);
			
			Assert.assertTrue(errors.isEmpty());
		}
		catch (ERLException e) {
			e.printStackTrace();
			Assert.assertTrue(false);
		}
	}
	
	
	
	@Test
	public void falseTest() {
		try {
			Oracle oracle = new TestOracle();
			Term andTerm = TermBuilder.createAndTerm(TermBuilder.createAtomicTerm("a"),TermBuilder.createAtomicTerm("b"));
			Term orTerm = TermBuilder.createOrTerm(TermBuilder.createAtomicTerm("b"), andTerm);
			
			List<ERLError> errors = ERL.runPredicate(oracle, andTerm, true);
			
			Assert.assertTrue(!errors.isEmpty());
		}
		catch (ERLException e) {
			e.printStackTrace();
			Assert.assertTrue(false);
		}
	}
}